FDL - Nuprl Lemma : ma-knows-true

Nuprl Lemma : ma-knows-true

11,40

poss:(ES{i}

{i'}), T:Type{i}, s:T, i:Id, P:(possible-event{i:l}(poss)

{i'}),

R:(possible-event{i:l}(poss)

possible-event{i:l}(poss)

{i'}), Rs:(T

{i'}).
(

e:possible-event{i:l}(poss). R(e,e))

ma-knows{i:l}

ma-knows(poss; i; T; s; P; Rs; R)

(

e:possible-event{i:l}(poss). poss-consistent(i;T;s;e;Rs)

(P(e)))

Definitions t T, P Q, x:A. B(x), K(P)@e, Type, , ES, x:AB(x), Id, PossibleEvent(poss), f(a), poss-consistent(i;T;s;ev;R), Ki(P)@s

Lemmas poss-consistent wf, es-knows wf, possible-event wf, Id wf, event system wf, es-knows-true

Definitions	t T, P Q, x:A. B(x), K(P)@e, Type, , ES, x:AB(x), Id, PossibleEvent(poss), f(a), poss-consistent(i;T;s;ev;R), Ki(P)@s
Lemmas	poss-consistent wf, es-knows wf, possible-event wf, Id wf, event system wf, es-knows-true